Nuprl Lemma : cons_neq_nil
11,40
postcript
pdf
T
:Type,
h
:
T
,
t
:(
T
List).
(cons(
h
;
t
) = [])
latex
Definitions
prop{i:l}
,
t
T
,
P
Q
,
A
,
x
:
A
.
B
(
x
)
,
False
origin
T:Type, h:T, t:(T List). 
(cons(h; t) = []) T:Type, h:T, t:(T List). (cons(h; t) = []) 
T
QAx:A. B(x)